import java.util.*;
import java.util.regex.*;

class TruthTableGenerator {
    // 运算符优先级（内部英文符号）：!> &> |> ->> <->
    private static final Map<Character, Integer> OP_PRIORITY = new HashMap<>();
    static {
        OP_PRIORITY.put('(', 0);
        OP_PRIORITY.put('<', 1);  // <-> 等价
        OP_PRIORITY.put('-', 2);  // -> 蕴含
        OP_PRIORITY.put('|', 3);  // | 析取
        OP_PRIORITY.put('&', 4);  // & 合取
        OP_PRIORITY.put('!', 5);  // ! 非
    }

    // 中文运算符到英文的映射
    private static final Map<String, String> CN_TO_EN_OP = new HashMap<>();
    static {
        CN_TO_EN_OP.put("¬", "!");
        CN_TO_EN_OP.put("∧", "&");
        CN_TO_EN_OP.put("∨", "|");
        CN_TO_EN_OP.put("→", "->");
        CN_TO_EN_OP.put("↔", "<->");
    }

    public static void main(String[] args) {
        Scanner scanner = new Scanner(System.in);
        System.out.println("请输入逻辑表达式（支持运算符：¬非、∧合取、∨析取、→蕴含、↔等价）");
        System.out.println("示例：(p∨¬q)∧(r→(s↔¬p))");
        String expression = scanner.nextLine().trim();
        scanner.close();

        try {
            // 1. 校验括号完整性
            if (!isBracketComplete(expression)) {
                throw new Exception("原始表达式括号不匹配，请检查括号成对情况");
            }

            // 2. 提取有效子表达式（保留中间子表达式，去重）
            List<String> subExpressions = extractValidSubExpressions(expression);
            // 添加最终表达式（去重）
            if (!subExpressions.contains(expression)) {
                subExpressions.add(expression);
            }

            // 3. 提取变元
            String normalizedExp = normalizeOperator(expression);
            Set<Character> variables = extractVariables(normalizedExp);
            if (variables.isEmpty()) {
                throw new Exception("未找到命题变元（如p、q、r等英文字母）");
            }
            List<Character> varList = new ArrayList<>(variables);
            varList.sort(Comparator.comparingInt(c -> Character.toLowerCase(c)));
            int rowCount = (int) Math.pow(2, varList.size());

            // 4. 输出表头
            printHeader(varList, subExpressions);

            // 5. 输出每行结果
            for (int i = 0; i < rowCount; i++) {
                Map<Character, Boolean> values = assignValues(varList, i);
                List<Boolean> results = new ArrayList<>();
                for (String subExp : subExpressions) {
                    String subNormalized = normalizeOperator(subExp);
                    if (!isBracketComplete(subNormalized.replace("->", "-").replace("<->", "<"))) {
                        throw new Exception("子表达式[" + subExp + "]括号不匹配");
                    }
                    results.add(evaluateExpression(subNormalized, values));
                }
                printRow(varList, values, results);
            }

            // 6. 判断公式类型
            String formulaType = getFormulaType(normalizedExp, varList);
            System.out.println("\n公式类型：" + formulaType);

        } catch (Exception e) {
            System.out.println("运行错误：" + e.getMessage());
        }
    }

    /**
     * 校验括号是否完整
     */
    private static boolean isBracketComplete(String exp) {
        int bracketCount = 0;
        for (char c : exp.toCharArray()) {
            if (c == '(') bracketCount++;
            else if (c == ')') {
                bracketCount--;
                if (bracketCount < 0) return false;
            }
        }
        return bracketCount == 0;
    }

    /**
     * 提取有效子表达式（保留中间子表达式，去重）
     */
    private static List<String> extractValidSubExpressions(String expression) {
        Set<String> validSubExp = new LinkedHashSet<>();
        Deque<String> stack = new LinkedList<>();
        stack.push(expression);

        while (!stack.isEmpty()) {
            String currentExp = stack.pop();
            // 过滤：长度≤1 或 纯变元（无运算符）的表达式
            if (currentExp.length() <= 1 || isPureVariable(currentExp)) {
                continue;
            }

            // 处理外层括号：如果外层有括号，先提取内层表达式（避免重复），再处理内层
            String processedExp = currentExp;
            if (currentExp.startsWith("(") && currentExp.endsWith(")") && isBracketComplete(currentExp)) {
                String innerExp = currentExp.substring(1, currentExp.length() - 1);
                if (!innerExp.isEmpty() && isBracketComplete(innerExp) && !isPureVariable(innerExp)) {
                    processedExp = innerExp; // 用内层表达式替代外层，避免重复
                    stack.push(innerExp); // 递归处理内层
                }
            }

            // 处理非运算（¬X）
            Pattern notPattern = Pattern.compile("^¬(.+)$");
            Matcher notMatcher = notPattern.matcher(processedExp);
            if (notMatcher.matches()) {
                String xExp = notMatcher.group(1);
                if (isBracketComplete(xExp) && !xExp.isEmpty() && !isPureVariable(processedExp)) {
                    validSubExp.add(processedExp); // 添加¬X
                    // 递归处理X（如果X不是纯变元）
                    if (!isPureVariable(xExp)) {
                        // 若X带外层括号，先处理为内层表达式
                        String xProcessed = xExp;
                        if (xExp.startsWith("(") && xExp.endsWith(")") && isBracketComplete(xExp)) {
                            xProcessed = xExp.substring(1, xExp.length() - 1);
                        }
                        validSubExp.add(xProcessed);
                        stack.push(xProcessed);
                    }
                }
                continue; // 避免重复处理为双目运算符
            }

            // 处理双目运算符（A op B），按优先级从低到高匹配（避免被高优先级运算符提前匹配）
            String[] binaryOpPatterns = {
                    "(.+)↔(.+)",  // 等价（最低优先级）
                    "(.+)→(.+)",  // 蕴含
                    "(.+)∨(.+)",  // 析取
                    "(.+)∧(.+)"   // 合取（较高优先级）
            };
            boolean matched = false;
            for (String patternStr : binaryOpPatterns) {
                Pattern pattern = Pattern.compile(patternStr);
                Matcher matcher = pattern.matcher(processedExp);
                if (matcher.matches()) {
                    String aExp = matcher.group(1);
                    String bExp = matcher.group(2);
                    // 校验A和B的括号完整性
                    if (isBracketComplete(aExp) && !aExp.isEmpty()
                            && isBracketComplete(bExp) && !bExp.isEmpty()
                            && !isPureVariable(processedExp)) {

                        validSubExp.add(processedExp); // 添加A op B
                        // 处理A（去除外层括号，避免重复）
                        String aProcessed = aExp;
                        if (aExp.startsWith("(") && aExp.endsWith(")") && isBracketComplete(aExp)) {
                            aProcessed = aExp.substring(1, aExp.length() - 1);
                        }
                        if (!isPureVariable(aProcessed)) {
                            validSubExp.add(aProcessed);
                            stack.push(aProcessed);
                        }
                        // 处理B（去除外层括号，避免重复）
                        String bProcessed = bExp;
                        if (bExp.startsWith("(") && bExp.endsWith(")") && isBracketComplete(bExp)) {
                            bProcessed = bExp.substring(1, bExp.length() - 1);
                        }
                        if (!isPureVariable(bProcessed)) {
                            validSubExp.add(bProcessed);
                            stack.push(bProcessed);
                        }
                        matched = true;
                        break; // 匹配到一个运算符后跳出，避免重复解析
                    }
                }
            }
            if (matched) {
                continue;
            }

            // 若未匹配到任何运算符，但包含运算符（可能是括号嵌套导致），直接添加并递归
            if (containsOperator(processedExp)) {
                validSubExp.add(processedExp);
                stack.push(processedExp);
            }
        }

        // 按计算顺序排序（从简单到复杂）
        List<String> sortedSubExp = new ArrayList<>(validSubExp);
        sortedSubExp.sort(Comparator.comparingInt(TruthTableGenerator::getExpressionComplexity));
        return sortedSubExp;
    }

    /**
     * 判断是否为纯变元（无任何运算符和括号，仅单个字母）
     */
    private static boolean isPureVariable(String exp) {
        return exp.matches("^[a-zA-Z]$");
    }

    /**
     * 判断表达式是否包含运算符
     */
    private static boolean containsOperator(String exp) {
        return exp.contains("¬") || exp.contains("∧") || exp.contains("∨") || exp.contains("→") || exp.contains("↔");
    }

    /**
     * 计算表达式复杂度（用于排序，值越小越简单）
     */
    private static int getExpressionComplexity(String exp) {
        // 运算符数量越多，复杂度越高
        int opCount = countOccurrences(exp, "¬") +
                countOccurrences(exp, "∧") +
                countOccurrences(exp, "∨") +
                countOccurrences(exp, "→") +
                countOccurrences(exp, "↔");
        // 括号深度越大，复杂度越高
        int bracketDepth = 0;
        int maxDepth = 0;
        for (char c : exp.toCharArray()) {
            if (c == '(') {
                bracketDepth++;
                maxDepth = Math.max(maxDepth, bracketDepth);
            } else if (c == ')') {
                bracketDepth--;
            }
        }
        return opCount * 10 + maxDepth; // 运算符权重更高
    }

    /**
     * 统计子串出现次数
     */
    private static int countOccurrences(String exp, String sub) {
        int count = 0;
        int index = 0;
        while ((index = exp.indexOf(sub, index)) != -1) {
            count++;
            index += sub.length();
        }
        return count;
    }

    /**
     * 提取命题变元
     */
    private static Set<Character> extractVariables(String expression) {
        Set<Character> variables = new HashSet<>();
        Pattern pattern = Pattern.compile("[a-zA-Z]");
        Matcher matcher = pattern.matcher(expression);
        while (matcher.find()) {
            variables.add(matcher.group().charAt(0));
        }
        return variables;
    }

    /**
     * 为变元分配真值
     */
    private static Map<Character, Boolean> assignValues(List<Character> variables, int row) {
        Map<Character, Boolean> values = new HashMap<>();
        int varCount = variables.size();
        for (int i = 0; i < varCount; i++) {
            int bitPosition = varCount - 1 - i;
            boolean value = ((row >> bitPosition) & 1) == 1;
            values.put(variables.get(i), value);
        }
        return values;
    }

    /**
     * 标准化运算符
     */
    private static String normalizeOperator(String exp) {
        String normalized = exp;
        for (Map.Entry<String, String> entry : CN_TO_EN_OP.entrySet()) {
            normalized = normalized.replace(entry.getKey(), entry.getValue());
        }
        return normalized;
    }

    /**
     * 计算表达式结果
     */
    private static boolean evaluateExpression(String normalizedExp, Map<Character, Boolean> values) throws Exception {
        List<String> postfix = infixToPostfix(normalizedExp);
        return evaluatePostfix(postfix, values);
    }

    /**
     * 中缀转后缀表达式
     */
    private static List<String> infixToPostfix(String exp) throws Exception {
        List<String> postfix = new ArrayList<>();
        Stack<Character> opStack = new Stack<>();
        int i = 0;
        int length = exp.length();

        while (i < length) {
            char c = exp.charAt(i);

            if (Character.isWhitespace(c)) {
                i++;
                continue;
            }

            if (Character.isLetter(c)) {
                postfix.add(String.valueOf(c));
                i++;
            } else if (c == '(') {
                opStack.push(c);
                i++;
            } else if (c == ')') {
                while (!opStack.isEmpty() && opStack.peek() != '(') {
                    postfix.add(String.valueOf(opStack.pop()));
                }
                if (opStack.isEmpty()) {
                    throw new Exception("括号不匹配：缺少左括号'('");
                }
                opStack.pop();
                i++;
            } else if (isOperator(c)) {
                if ((c == '-' && i + 1 < length && exp.charAt(i + 1) == '>') ||
                        (c == '<' && i + 2 < length && exp.charAt(i + 1) == '-' && exp.charAt(i + 2) == '>')) {

                    String opStr;
                    if (c == '-') {
                        opStr = "->";
                        i += 2;
                    } else {
                        opStr = "<->";
                        i += 3;
                    }
                    while (!opStack.isEmpty() && OP_PRIORITY.get(opStack.peek()) >= OP_PRIORITY.get(opStr.charAt(0))) {
                        postfix.add(String.valueOf(opStack.pop()));
                    }
                    opStack.push(opStr.charAt(0));
                } else {
                    while (!opStack.isEmpty() && OP_PRIORITY.get(opStack.peek()) >= OP_PRIORITY.get(c)) {
                        postfix.add(String.valueOf(opStack.pop()));
                    }
                    opStack.push(c);
                    i++;
                }
            } else {
                throw new Exception("无效字符：'" + c + "'");
            }
        }

        while (!opStack.isEmpty()) {
            char op = opStack.pop();
            if (op == '(') {
                throw new Exception("括号不匹配：缺少右括号')'");
            }
            postfix.add(String.valueOf(op));
        }

        return postfix;
    }

    /**
     * 计算后缀表达式
     */
    private static boolean evaluatePostfix(List<String> postfix, Map<Character, Boolean> values) throws Exception {
        Stack<Boolean> stack = new Stack<>();

        for (String token : postfix) {
            if (token.length() == 1 && isOperator(token.charAt(0))) {
                char op = token.charAt(0);
                if (op == '!') {
                    if (stack.isEmpty()) throw new Exception("非运算符缺少操作数");
                    stack.push(!stack.pop());
                } else {
                    if (stack.size() < 2) throw new Exception("双目运算符缺少操作数");
                    boolean b = stack.pop();
                    boolean a = stack.pop();
                    switch (op) {
                        case '&': stack.push(a && b); break;
                        case '|': stack.push(a || b); break;
                        case '-': stack.push(!a || b); break;
                        case '<': stack.push(a == b); break;
                        default: throw new Exception("未知运算符：" + op);
                    }
                }
            } else if (token.length() == 1 && Character.isLetter(token.charAt(0))) {
                char var = token.charAt(0);
                if (!values.containsKey(var)) throw new Exception("未知变元：" + var);
                stack.push(values.get(var));
            } else {
                throw new Exception("无效表达式元素：" + token);
            }
        }

        if (stack.size() != 1) throw new Exception("表达式错误");
        return stack.pop();
    }

    /**
     * 判断是否为运算符
     */
    private static boolean isOperator(char c) {
        return c == '!' || c == '&' || c == '|' || c == '-' || c == '<';
    }

    /**
     * 输出表头
     */
    private static void printHeader(List<Character> variables, List<String> subExpressions) {
        // 打印变元列（每个占4字符）
        for (char var : variables) {
            System.out.printf("%4c", var);
        }
        // 打印子表达式列（每个占15字符，根据长度调整）
        for (String subExp : subExpressions) {
            System.out.printf("%15s", subExp);
        }
        System.out.println();

        // 打印分隔线
        for (int i = 0; i < variables.size(); i++) {
            System.out.print("----");
        }
        for (int i = 0; i < subExpressions.size(); i++) {
            System.out.print("---------------");
        }
        System.out.println();
    }

    /**
     * 输出行
     */
    private static void printRow(List<Character> variables, Map<Character, Boolean> values, List<Boolean> results) {
        // 打印变元真值
        for (char var : variables) {
            System.out.printf("%4d", values.get(var) ? 1 : 0);
        }
        // 打印子表达式结果
        for (boolean res : results) {
            System.out.printf("%15d", res ? 1 : 0);
        }
        System.out.println();
    }

    /**
     * 判断公式类型
     */
    private static String getFormulaType(String expression, List<Character> variables) throws Exception {
        int rowCount = (int) Math.pow(2, variables.size());
        boolean allFalse = true, allTrue = true;
        for (int i = 0; i < rowCount; i++) {
            boolean res = evaluateExpression(expression, assignValues(variables, i));
            if (res) allFalse = false;
            if (!res) allTrue = false;
        }
        if (allFalse) return "矛盾式（所有情况均为假）";
        if (allTrue) return "重言式（所有情况均为真）";
        return "可满足式（存在至少一种情况为真）";
    }
}